Step of Proof: equiv_rel_functionality_wrt_iff 12,41
Inference at * 1 1 0 
Iof proof for Lemma equiv rel functionality wrt iff:



1. T : Type
2. T' : Type
3. E : TT
4. E' : T'T'
5. T = T'
6. x, y:T. E(x,y)  E'(x,y)
  ((a:T. E(a,a)) & (a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c)))
   ((a:T'. E'(a,a))
   & (a, b:T'. E'(a,b)  E'(b,a))
   & (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c))) 
latex
 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{12:n,
 by PERMUTE{8:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{8:n,
 by PERMUTE{8:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{11:n,
 by PERMUTE{19:n,
 by PERMUTE{19:n,
 by PERMUTE{20:n,
 by PERMUTE{21:n,
 by PERMUTE{22:n,
 by PERMUTE{23:n,
 by PERMUTE{24:n,
 by PERMUTE{25:n,
 by PERMUTE{26:n,
 by PERMUTE{27:n,
 by PERMUTE{28:n,
 by PERMUTE{28:n,
 by PERMUTE{27:n,
 by PERMUTE{19:n,
 by PERMUTE{8:n,
 by PERMUTE{8:n,
 by PERMUTE{8:n,
 by PERMUTE{29:n,
 by PERMUTE{30:n,
 by PERMUTE{11:n,
 by PERMUTE{19:n,
 by PERMUTE{19:n,
 by PERMUTE{31:n,
 by PERMUTE{32:n,
 by PERMUTE{22:n,
 by PERMUTE{33:n,
 by PERMUTE{33:n,
 by PERMUTE{34:n,
 by PERMUTE{35:n,
 by PERMUTE{36:n,
 by PERMUTE{37:n,
 by PERMUTE{38:n,
 by PERMUTE{39:n,
 by PERMUTE{40:n,
 by PERMUTE{41:n,
 by PERMUTE{42:n,
 by PERMUTE{43:n,
 by PERMUTE{44:n,
 by PERMUTE{45:n,
 by PERMUTE{46:n,
 by PERMUTE{42:n,
 by PERMUTE{47:n,
 by PERMUTE{41:n,
 by PERMUTE{47:n,
 by PERMUTE{33:n,
 by PERMUTE{19:n,
 by PERMUTE{8:n,
 by PERMUTE{48:n,
 by PERMUTE{49:n} 
latex

 1: .....wf..... NILNIL

 1:   ((a:T. E(a,a)) & (a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c)))
 1:    
 2: .....wf..... NILNIL

 2:   ((a:T. E'(a,a))
 2:   (& (a, b:T. E'(a,b)  E'(b,a))
 2:   (& (a, b, c:T. E'(a,b)  E'(b,c)  E'(a,c)))
 2:    
 3: .....wf..... NILNIL

 3:   ((a:T'. E'(a,a))
 3:   (& (a, b:T'. E'(a,b)  E'(b,a))
 3:   (& (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c)))
 3:    
 4: .....wf..... NILNIL

 4:   (a:T. E(a,a))  
 5: .....wf..... NILNIL

 5:   (a:T. E'(a,a))  
 6: .....wf..... NILNIL

 6:   ((a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c)))  
 7: .....wf..... NILNIL

 7:   ((a, b:T. E'(a,b)  E'(b,a)) & (a, b, c:T. E'(a,b)  E'(b,c)  E'(a,c)))  
 8: .....wf..... NILNIL

 8:   T  Type
 9: .....wf..... NILNIL

 9:   (a.E(a,a))  T
 10: .....wf..... NILNIL

 10:   (a.E'(a,a))  T
 11: .....wf..... NILNIL

 11:   T = T
 12: .....wf..... NILNIL

 12: 7. a : T
 12:   a  T
 13: .....wf..... NILNIL

 13:   (a, b:T. E(a,b)  E(b,a))  
 14: .....wf..... NILNIL

 14:   (a, b:T. E'(a,b)  E'(b,a))  
 15: .....wf..... NILNIL

 15:   (a, b, c:T. E(a,b)  E(b,c)  E(a,c))  
 16: .....wf..... NILNIL

 16:   (a, b, c:T. E'(a,b)  E'(b,c)  E'(a,c))  
 17: .....wf..... NILNIL

 17:   (a.b:T. E(a,b)  E(b,a))  T
 18: .....wf..... NILNIL

 18:   (a.b:T. E'(a,b)  E'(b,a))  T
 19: .....wf..... NILNIL

 19: 7. T
 19:   T  Type
 20: .....wf..... NILNIL

 20: 7. a : T
 20:   (b.E(a,b)  E(b,a))  T
 21: .....wf..... NILNIL

 21: 7. a : T
 21:   (b.E'(a,b)  E'(b,a))  T
 22: .....wf..... NILNIL

 22: 7. T
 22:   T = T
 23: .....wf..... NILNIL

 23: 7. a : T
 23: 8. b : T
 23:   E(a,b)  
 24: .....wf..... NILNIL

 24: 7. a : T
 24: 8. b : T
 24:   E'(a,b)  
 25: .....wf..... NILNIL

 25: 7. a : T
 25: 8. b : T
 25:   E(b,a)  
 26: .....wf..... NILNIL

 26: 7. a : T
 26: 8. b : T
 26:   E'(b,a)  
 27: .....wf..... NILNIL

 27: 7. a : T
 27: 8. T
 27:   a  T
 28: .....wf..... NILNIL

 28: 7. T
 28: 8. b : T
 28:   b  T
 29: .....wf..... NILNIL

 29:   (a.b, c:T. E(a,b)  E(b,c)  E(a,c))  T
 30: .....wf..... NILNIL

 30:   (a.b, c:T. E'(a,b)  E'(b,c)  E'(a,c))  T
 31: .....wf..... NILNIL

 31: 7. a : T
 31:   (b.c:T. E(a,b)  E(b,c)  E(a,c))  T
 32: .....wf..... NILNIL

 32: 7. a : T
 32:   (b.c:T. E'(a,b)  E'(b,c)  E'(a,c))  T
 33: .....wf..... NILNIL

 33: 7. T
 33: 8. T
 33:   T  Type
 34: .....wf..... NILNIL

 34: 7. a : T
 34: 8. b : T
 34:   (c.E(a,b)  E(b,c)  E(a,c))  T
 35: .....wf..... NILNIL

 35: 7. a : T
 35: 8. b : T
 35:   (c.E'(a,b)  E'(b,c)  E'(a,c))  T
 36: .....wf..... NILNIL

 36: 7. T
 36: 8. T
 36:   T = T
 37: .....wf..... NILNIL

 37: 7. a : T
 37: 8. b : T
 37: 9. T
 37:   E(a,b)  
 38: .....wf..... NILNIL

 38: 7. a : T
 38: 8. b : T
 38: 9. T
 38:   E'(a,b)  
 39: .....wf..... NILNIL

 39: 7. a : T
 39: 8. b : T
 39: 9. c : T
 39:   (E(b,c)  E(a,c))  
 40: .....wf..... NILNIL

 40: 7. a : T
 40: 8. b : T
 40: 9. c : T
 40:   (E'(b,c)  E'(a,c))  
 41: .....wf..... NILNIL

 41: 7. a : T
 41: 8. T
 41: 9. T
 41:   a  T
 42: .....wf..... NILNIL

 42: 7. T
 42: 8. b : T
 42: 9. T
 42:   b  T
 43: .....wf..... NILNIL

 43: 7. T
 43: 8. b : T
 43: 9. c : T
 43:   E(b,c)  
 44: .....wf..... NILNIL

 44: 7. T
 44: 8. b : T
 44: 9. c : T
 44:   E'(b,c)  
 45: .....wf..... NILNIL

 45: 7. a : T
 45: 8. T
 45: 9. c : T
 45:   E(a,c)  
 46: .....wf..... NILNIL

 46: 7. a : T
 46: 8. T
 46: 9. c : T
 46:   E'(a,c)  
 47: .....wf..... NILNIL

 47: 7. T
 47: 8. T
 47: 9. c : T
 47:   c  T
 48: .....wf..... NILNIL

 48:   ((a:T'. E'(a,a))
 48:   (& (a, b:T'. E'(a,b)  E'(b,a))
 48:   (& (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c)))
 48:   =
 48:   ((a:T'. E'(a,a))
 48:   (& (a, b:T'. E'(a,b)  E'(b,a))
 48:   (& (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c)))
 49: 

 49:   ((a:T. E'(a,a))
 49:   & (a, b:T. E'(a,b)  E'(b,a))
 49:   & (a, b, c:T. E'(a,b)  E'(b,c)  E'(a,c)))
 49:    ((a:T'. E'(a,a))
 49:    & (a, b:T'. E'(a,b)  E'(b,a))
 49:    & (a, b, c:T'. E'(a,b)  E'(b,c)  E'(a,c)))
 .

Definitionst  T, x:A  B(x), x.A(x), f(a), x(s1,s2), s = t, , x:AB(x), Type, {T}, x(s), x. t(x), P  Q, P  Q, P & Q, P  Q, x:A. B(x)
Lemmasimplies functionality wrt iff, all functionality wrt iff, and functionality wrt iff, iff functionality wrt iff

origin